COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 LISP lambda calculus functions
C00009 00003	 Simulating LISP in λ-calculus involves using certain λ-expressions
C00011 00004	 A few recursive definitions.
C00012 ENDMK
C⊗;
;;; LISP lambda calculus functions

;;; We begin with syntactic functions for λ-expressions.

(macrodef isvar (e) (and (atom e) (null (assoc e abbrevs))))

(macrodef islam (e) (and (not (atom e)) (eq (car e) 'λ)))

(macrodef bvars (e) (cadr e))

(macrodef body (e) (caddr e))

(macrodef mklam (bvars body) (list 'λ bvars body))

(macrodef fun (e) (car e))

(macrodef args (e) (cdr e))

(macrodef mkap (fun args) (cons fun args))


;;;Does λ-conversion and also substitutes when necessary the values
;;;of abbreviations.

(defun convert (e) (if
(isvar e) e
;;;(atom e) (val e)
(isvar (fun e)) e
(atom (fun e))
(mkap (val (fun e)) (args e))
(islam (fun e))
	   (IF (NULL (bvars (FUN E)))
			  (BODY (FUN E))
			  (NULL (args E))
			  (FUN E)
			  (MKAP (SUBLAM (CAR (args E))
					(CAR (bvars (FUN E)))
					(MKLAM (CDR (bvars (FUN E)))
					       (BODY (FUN E))))
				(CDR (args E))))
(mkap (convert (fun e)) (args e))
))

;;; Converts until it can't convert any more.  It does all possible
;;;conversions at the outer level before converting inside.  This is
;;;necessary to insure termination as often as possible and corresponds
;;;to call-by-name evaluation.  This rather impure LISP isn't really
;;;necesary.

(defun normalize (e) (prog (w)
	(setq w e)
loop	(if
		(not (equal w (setq w (convert w))))
		(go loop)
		(return (if
				(or (isvar w) (atom w))
				w
				(islam w)
				(mklam (bvars w) (normalize (body w)))
				(mkap	(normalize (fun w))
					(normalizelist (args w)))
)))))

(defun normalizelist (u) (if (null u) nil
			(cons (normalize (car u)) (normalizelist (cdr u)))))

;;; sublam is like subst but it must modify the bound variable of the
;;; expression into which it is substituting if necessary to avoid
;;; capture of free variables in the expression being substituted.
;;; It isn't clear that sublam is would be needed for the simulation
;;; of LISP, when the functions are LISP functions and the arguments
;;; have no free variables, but we haven't proved that no free variables
;;; can be captured.  If not, subst could be used instead, which would
;;; make it much easier to prove properties of a purified version of
;;; normalize.

(defun sublam (x y z) (sublam1 x y z (freevars x)))

(defun sublam1 (x y z w) (if
	(isvar z)
	(if (equal y z) x z)
	(atom z)
	z
	(not (islam z))
	(mkap (sublam1 x y (fun z) w) (sublamlis x y (args z) w))
	(member y (bvars z))
	z
	(sublam2 x y z w (intersection w (bvars z)))))

(defun sublamlis (x y u w) (if
	(null u)
	nil
	(cons (sublam1 x y (car u) w) (sublamlis x y (cdr u) w))
))

(defun intersection (u v) (if
	(null u)
	nil
	(member (car u) v)
	(cons (car u) (intersection (cdr u) v))
	(intersection (cdr u) v)
))

(defun union (u v) (append u v))


(defun sublam2 (x y z w u) (if 
		(null u) 
		(mklam (bvars z) (sublam1 x y (body z) w))
		((lambda (newsym) (sublam2 x y 
(mklam (subst newsym (car u) (bvars z)) (subst newsym (car u) (body z)))
w (cdr u))) (gensym))
))


;;; The free variables of a λ-calculus expression.

(defun freevars (e) (freevars1 e nil nil))

(defun freevars1 (e bound sofar) (if
	(isvar e)
	(if (or (member e bound) (member e sofar)) sofar (cons e sofar))
	(atom e)
	nil
	(islam e)
	(freevars1 (body e) (union (bvars e) (body e)) sofar)
	(freevars1list (args e) bound (freevars1 (fun e) bound sofar))
))

(defun freevars1list (u bound sofar) (if
	(null u)
	sofar
	(freevars1list (cdr u) bound (freevars1 (car u) bound sofar))
))

;;; This is a pure version of normalize which is just as efficient
;;;  as normalize  if compiled iteratively.  However, it still has
;;; the impurity of using  sublam  which uses  gensym.

(defun normalize1 (e) ((lambda (w) (if
	(equal w e)
	(if 
		(or (isvar e) (atom e))
		e
		(islam e)
		((lambda (w) (if
			(equal w (body e))
			e
			(mklam (bvars e) w)))
		 (convert (body e)))
		(mkap (normalize1 (fun e)) (normalize1list (args e)))
	)
	(normalize1 w)))
(convert e)))

(defun normalize1list (u) (if (null u) nil
			(cons (normalize1 (car u)) (normalize1list (cdr u)))))
;;; Simulating LISP in λ-calculus involves using certain λ-expressions
;;; for true, false, car, cdr, cons, cond, etc.  They are defined successively
;;; and get very long if written out.  Therefore, we provide the following
;;; abbreviations, and the function  normalize and its satellites expand
;;; them out only as needed.

(setq abbrevs nil)

;;; The imbedded setq here is present only to aid debugging and experimentation.
(defun adf (name val) (prog nil (set name val) 
(setq abbrevs (cons (cons name val) abbrevs))))

(defun val (e) (cdr (assoc e abbrevs)))

(adf 'true '(λ (x y) x))
(adf 'false '(λ (x y) y))
(adf 'if '(λ (x y z) (x y z)))

(adf 'and '(λ (x y) (if x y false)))
(adf 'or  '(λ (x y) (if x true y)))
(adf 'not '(λ (x) (if x false true)))

(adf 'cons1 '(λ (x y z) (z x y)))
(adf 'car1 '(λ (z) (z true)))
(adf 'cdr1 '(λ (z) (z false)))

;;; recur is Church's famous Y combinator.
(adf 'recur '(λ (z) ((λ (x) (z (x x))) (λ (x) (z (x x))))))

(adf 'cons '(λ (x y) (cons1 false (cons1 x y))) )
(adf 'car '(λ (x) (car1 (cdr1 x))) )
(adf 'cdr '(λ (x) (cdr1 (cdr1 x))) )
(adf 'null '(λ (x) (car1 x)) )

;;; There would be trouble if we spelled it nil.
(adf 'nl '(cons1 true true) )
;;; A few recursive definitions.

(adf 'append '(recur (λ (z x y) ((null x) y (cons (car x) (z (cdr x) y))))))

(adf 'ff '(recur (λ (y x) ((null x) nl (y (car x))))))

(adf 'equal '(recur (λ (z x y)
	(or (and (null x) (null y))
		(and (and (not (null x)) (not (null y)))
			(and (z (car x) (car y)) (z (cdr x) (cdr y))))))))

(adf 'equal1 '(recur (λ (z x y) (if
	(null x)
	(null y)
	(if
		(null y)
		false
		(if	(z (car x) (car y))
			(z (cdr x) (cdr y))
			false
		)
	)
))))